M1, M2:MsgA. M1  M2  (a:Id. a declared in M1  a declared in M2) 

latex

Definitions	locl(a), a declared in M, M1  M2, MsgA, Valtype(da;k), P & Q, b, x  dom(f), KindDeq, a:A fp B(a), x. t(x), IdLnk, f  g, P  Q, x:A. B(x), Knd, Id, t  T, A & B
Lemmas	locl wf, Knd wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, assert wf, Id wf, ma-sub wf, msga wf